A:Type, B:(AType), f,g:fpf(A; a.B(a)), eq:EqDecider(A). fpf-join(eq; f; g)  fpf(A; a.B(a)) 

latex

Definitions	x:A. B(x), fpf(A; a.B(a)), x(s), t  T, fpf-join(eq; f; g), x. t(x), fpf-cap(f; eq; x; z), if b then t else f fi , P  Q, tt, ff, prop{i:l}, fpf-dom(eq; x; f), , Unit, P  Q, P  Q, P  Q, A, False, P  Q,
Lemmas	append wf, pi1 wf, l member wf, filter wf, bnot wf, fpf-dom wf, fpf-trivial-subtype-top, deq wf, bool wf, eqtt to assert, iff transitivity, assert wf, not wf, eqff to assert, assert of bnot, fpf-ap wf, member append, deq-member wf, not functionality wrt iff, assert-deq-member, member filter